Step of Proof: equiv_rel_self_functionality 12,41
Inference at * 1 1 1 
Iof proof for Lemma equiv rel self functionality:



1. T : Type
2. R : TT
3. a:T. R(a,a)
4. a, b:T. R(a,b)  R(b,a)
5. a, b, c:T. R(a,b)  R(b,c)  R(a,c)
6. a : T
7. a' : T
8. b : T
9. b' : T
10. R(a,b)
11. R(a',b')
12. R(a,a')
  R(b,b') 
latex
 by ((((((FHyp 4 [10]) 
CollapseTHENM (FHyp 5 [13;12]))) 
CollapseTHENM (FHyp 5 [14;11]))) 

CoCollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t
C) inil_term))) 
latex

C.

Definitionst  T, P  Q, x:A. B(x)

origin